L:Dsys List.
(A,BL.A || B)
 (M:Dsys. (BL. interface-compatible(M;B))  interface-compatible(M;(L))) 

latex

Definitions	A  B, x,y. t(x;y), P  Q, {T}, (x,yL.P(x;y)), , xL. P(x), x. t(x), interface-compatible(A;B), Prop, A || B, l[i], MsgA, Id, {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, x:A. B(x), t  T, (L), Dsys
Lemmas	dsys wf, interface-compatible-null, select wf, msga wf, Id wf, m-sys-compatible wf, int seg wf, length wf2, interface-compatible wf, l all wf, dsys-join-list-property, interface-compatible-join, l all cons, pairwise-cons, pairwise wf